2018-06-08

Расширения Кана

Вчера весь вечер рисовал страницу про категории и крутил расширения Кана. Так и не смог построить даже сигнатуру универсальности расширений Кана, вот лох! Но обо всем по порядку. Расширение Кана двух функторов К: А -> B, G: A -> C — это такой функтор F: B -> C, для которого существует естественное преобразование композиции функоторов F o K и функтора G. Конус функтора D: J -> C — это расширение кана, где функтор К: J -> 1 действует в кодомен единичной категории. Свойство универсальности расширений Кана — это их единственность при фиксации К и G для любых двух расширений Кана. Правое расширение Кана функторов К и G, это по-сути определение расширения Кана вместе со свойством универсальности, т.е. ∑ (x: extension K G) ∏ (y: extension K G) isContr(universality K G x y). Категорный предел по функтору D: J -> C (диаграмме) — есть правое раширение Кана, где К: J -> 1 действует в единичную категорию. Вот и все.


 extension (A B C: precategory) (K: catfunctor A B) (G: catfunctor A C) : U
    = (F: catfunctor B C)
    * (counit: ntrans A C (compFunctor A B C K F) G)
    * unit

Functor to Unit Category


 unitFunc (C: precategory): catfunctor C unitCat
    = undefined

Cone as Kan Extension


 cone (J C: precategory) (D: catfunctor J C): U
   = extension J unitCat C (unitFunc J) D

universality of Kan Extension


 universality (A B C: precategory)
              (K: catfunctor A B) (G: catfunctor A C) 
              (s t: extension A B C K G) : U

Right Kan Extension


 ran (A B C: precategory) (K: catfunctor A B) (G: catfunctor A C) : U
    = (x: extension A B C K G) * ((y: extension A B C K G)
    -> isContr (universality A B C K G x y))

Limit


 limit (J C: precategory) (D: catfunctor J C): U
    = ran J unitCat C (unitFunc J) D

[1]. http://www.math.harvard.edu/theses/senior/lehner/lehner.pdf
[2]. https://github.com/groupoid/cubical/blob/master/src/cat.ctt
[3]. https://github.com/groupoid/cubical/blob/master/src/fun.ctt
[4]. https://github.com/groupoid/cubical/blob/master/src/adj.ctt
[5]. https://github.com/groupoid/cubical/blob/master/src/sip.ctt
[6]. https://github.com/groupoid/cubical/blob/master/src/cones.ctt